\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$, ${\it triggerV}$:Type, $l$:IdLnk, ${\it tg}$:Id, ${\it knd}$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it cond}$:(State(${\it ds}$)$\rightarrow$${\it triggerV}$$\rightarrow$($A$ + Top)).
\-\\[0ex]($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (valtype($e$) $\subseteq$r $A$))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex](loc($e$) = source($l$) $\in$ Id)
\\[0ex]$\Rightarrow$ (kind($e$) = ${\it knd}$)
\\[0ex]$\Rightarrow$ ((valtype($e$) $\subseteq$r ${\it triggerV}$) \& (state@loc($e$) $\subseteq$r State(${\it ds}$))))
\-\\[0ex]$\Rightarrow$ \=($\forall$$p$:(\=$\forall$$e$:E.\+\+
\\[0ex]Dec(($\uparrow$isrcv($e$))
\\[0ex]\& lnk($e$) = $l$
\\[0ex]\& loc(sender($e$)) = source($l$) $\in$ Id
\\[0ex]\& kind(sender($e$)) = ${\it knd}$)).
\-\\[0ex]${\it knd}$(v:${\it triggerV}$) sends on $l$ [${\it tg}$:$A$, $\lambda$$p$.let $s$,$v$ = $p$ in ${\it cond}$($s$,$v$) $<$state, v$>$]?[]
\\[0ex]$\Rightarrow$ glues(\=${\it es}$;\+
\\[0ex]$A$;
\\[0ex]($\lambda$$e$.sender($e$));
\\[0ex]($\lambda$$e$.outl(${\it cond}$((state when $e$),val($e$))));
\\[0ex]es{-}trigger(${\it es}$;source($l$);${\it knd}$;${\it ds}$;${\it cond}$);
\\[0ex](es{-}in{-}port(${\it es}$;$l$;${\it tg}$)$\mid$$p$)))
\-\-
\end{tabbing}